/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */


package ch.epfl.lara.patterns.analyze;

import ch.epfl.lara.patterns.ast.{Formula,Or,And,True,False}

/**
 * <p>
 *   FormulaWrapper wraps a given list of formulas in a unique formula in 
 *   either CNF or DNF form.
 * </p>
 */
trait FormulaWrapper {

  /**
   * <p> 
   * 	Merge a List of formulas to a unique formula in DNF.
   * </p>
   * @param formulas: The list of formulas
   * @return: A formula that is in DNF
   */
  protected def DNF(formulas: List[Formula]) : Formula = 
    if(formulas.isEmpty)
      False
    else
      formulas.reduceRight[Formula]( (formula, dnf) => Or(formula,dnf) )
      
    
  /**
   * <p>
   * 	Merge a List of formulas to a unique formula in CNF.
   * </p>
   * @param formulas: The list of formulas
   * @return: A formula that is in CNF
   */
  protected def CNF(formulas: List[Formula]) : Formula = 
    if(formulas.isEmpty)
      True
    else
      formulas.reduceRight[Formula] ( (formula, cnf) => And(formula,cnf) )
}
